#include <QtGui>

#include "PDTCheckSpecMainWindow.h"
#include "PDTCodeGraph.h"
#include "PDTCheckSpec.h"
#include <string>

using namespace std;

unsigned int 
PDTSpecTriple::numChildren() const {
    unsigned int rc = 0;
    if (pre ) rc++;
    if (post) rc++;
    if (behaviors) rc++;
    return rc;
}

const string & PDTSpecTriple::name() const{
    if (pre)
        return pre->getName();
    if (post)
        return post->getName();
    if (behaviors)
        return behaviors->getName();
    assert(false);
    return "";
}

/*
   level = 0: specTripleItem
   level = 1, row = 0: pre item
   level = 1, row = 1: post item
   level = 1, row = 2: behaviors item
   level = 2, row = i: i-th behavior item
   level = 3, row = 0: input item
   level = 3, row = 1: output item
   */


PDTNode * 
PDTSpecTriple::getNodeFromRow(unsigned int row) const
{
    if (row >= numChildren())
        return NULL;
    if (row == 0) {
        if (pre != NULL) 
            return pre;
        if (post != NULL)
            return post;
        if (behaviors != NULL)
            return behaviors;
    }
    if (row == 1) {
        if (pre != NULL) {
            if (post != NULL)
                return post;
            return behaviors;
        }
        if (post != NULL)
            return behaviors;
        return post;
    }
    if (row == 2) 
        return behaviors;
    return NULL;
}
#if 1
        /*
           good/bad   number
             advice   text! 
             p(i)     true/false
             q(i,o)   true/false
             q(i,o')  true/false   --- if with code
             o == o'  true/false   --- if with code
             values                
                var   value-of-var

           */
QVariant ResultItemModel :: headerData(int section, 
        Qt::Orientation orientation, int role) const 
{
    if (orientation == Qt::Horizontal && role == Qt::DisplayRole)
    {
        if (section == 0)
            return QVariant("Label");
        if (section == 1)
            return QVariant("Value");
    }
    return QVariant();
}
int ResultItemModel :: rowCount(const QModelIndex &parent ) const 
{
    if (!parent.isValid())
        return cSpecMW.results.size();
    IID id =  parent.internalId();
    switch (id.type) {
        case BehaviorItem: // the parent is a behavior item
            return id.withCode ? 6 : 4;
            break;
        case AdviceItem:
        case PofIItem:
        case QofIOItem:
        case QofIOprimeItem:
        case OeqOprimeItem:
            return 0;
            break;
        case ValuesItem:
        {
            vector<PDTVar *> & vars = cSpecMW.resultVars[id.resultId];
            return vars.size();
        }
            break;
        case VarItem:
            return 0;
        break;
    };
    return 0;
}
int ResultItemModel :: columnCount(const QModelIndex &parent) const 
{
    return 2;
}
QModelIndex ResultItemModel :: parent(const QModelIndex &index) const
{
    if (!index.isValid())
        return QModelIndex();
    IID id =  index.internalId();
    switch(id.type) {
        case BehaviorItem: // the parent is a behavior item
            break;
        case AdviceItem:
        case PofIItem:
        case QofIOItem:
        case QofIOprimeItem:
        case OeqOprimeItem:
        case ValuesItem:
            assert (id.resultId < cSpecMW.results.size());
        {
            IID parentId(BehaviorItem, id.resultId, id.withCode);
            return createIndex(id.resultId, 0, parentId.uint());
        }
            break;
        case VarItem:
        {
            vector<PDTVar *> & vars = cSpecMW.resultVars[id.resultId];
            if (index.row() < vars.size()) {
                IID parentId(ValuesItem, id.resultId, id.withCode);
                unsigned int parentRow = (id.withCode == 1) ? 5 : 3;
                return createIndex(parentRow, 0, parentId.uint());
            }
        }
        break;
    }
    return QModelIndex();
}

QVariant ResultItemModel :: data(const QModelIndex &index, int role) const
{
    if (!index.isValid())
        return QVariant();
    if (role != Qt::DisplayRole)
        return QVariant();
    if (index.column() > 1) 
        return QVariant();

    IID id =  index.internalId();
    unsigned int col = index.column();
    unsigned int row = index.row();
    PDTCheckSpec::Result & res = cSpecMW.results[id.resultId];

    switch (id.type) {
        case BehaviorItem: // the parent is a behavior item
            assert(row == id.resultId);
            if (col == 0) {
                PDTBehavior * beh = res.beh;

                string str = res.withCode ? "{P}S{Q}{B}" : "{P}-{Q}{B}";
                if (beh->isGood()) {
                    str += " good";
                } else {
                    str += " bad";
                }
                return QVariant(str.c_str());
            } else { 
                if (res.pass()) {
                    return QVariant("pass");
                } else {
                    return QVariant("fail");
                }
            }
            break;
        case AdviceItem:
            assert(row == 0);
            if (col == 0) {
                return QVariant("advice");
            } else { 
                return QVariant(res.advice().c_str());
            }
            break;
        case PofIItem:
            assert(row == 1);
            if (col == 0) {
                return QVariant("P(i)");
            } else  {
                return QVariant((bool)res.PofI);
            }
            break;
        case QofIOItem:
            assert(row == 2);
            if (col == 0) {
                return QVariant("Q(i,o)");
            } else  {
                return QVariant((bool)res.QofO);
            }
            break;
        case QofIOprimeItem:
            assert(row == 3);
            if (col == 0) {
                return QVariant("Q(i,o')");
            } else  {
                return QVariant((bool)res.QofOPrime);
            }
            break;
        case OeqOprimeItem:
            assert(row == 4);
            if (col == 0) {
                return QVariant("o' in g(i)");
            } else  {
                return QVariant((bool)res.oEqOPrime);
            }
            break;
        case ValuesItem:
            assert(res.withCode ? row == 5 : row == 3);
            if (col == 0) 
                return QVariant("Values");
            else {
                vector<PDTVar *> & vars = cSpecMW.resultVars[id.resultId];
                unsigned int size = vars.size();
                return QVariant(size);
            }
            break;
        case VarItem:{
                vector< PDTVar *> & vars = cSpecMW.resultVars[id.resultId];
                if (row < vars.size()) {
            assert(row == id.varId);
            if (col == 0) {
                assert(row <vars.size());
                PDTVar * var = vars[id.varId];
                string name = var->getName();
                return QVariant(name.c_str());
            } else  {
                vector< PDTConst *> & values = cSpecMW.resultValues[id.resultId];
                assert(row < values.size());
                PDTConst * val = values[id.varId];
                stringstream ss;
                val->getNode()->toString(ss);
                return QVariant(ss.str().c_str());
            } 
                     }
                     }
        break;
    }
    return QVariant();
}


Qt::ItemFlags ResultItemModel :: flags(const QModelIndex &index) const
{
    if (!index.isValid())
        return 0;

    return Qt::ItemIsEnabled | Qt::ItemIsSelectable;

}

QModelIndex ResultItemModel :: index(int row, int column,
            const QModelIndex &parent ) const
{
    if (!hasIndex(row, column, parent))
        return QModelIndex();

    if (column >= 2) 
        return QModelIndex();

    if (!parent.isValid()) {
        if (row < cSpecMW.results.size()){
            PDTCheckSpec::Result & res = cSpecMW.results[row];
            IID myid (BehaviorItem,row,res.withCode);
            return createIndex(row, column, myid.uint());
        }
        return QModelIndex();
    }
    IID parentId =  parent.internalId();
    assert(parentId.resultId < cSpecMW.results.size());

    switch(parentId.type) {
        case BehaviorItem: // the parent is a behavior item
            if (parentId.withCode) {
                if (row < 6) {
                    ItemType types[6] = {AdviceItem,PofIItem,QofIOItem,QofIOprimeItem,OeqOprimeItem,ValuesItem};
                    IID myid(types[row], parentId.resultId, true);
                    return createIndex(row, column, myid.uint());
                }
            } else {
                if (row < 4) {
                    ItemType types[4] = {AdviceItem,PofIItem,QofIOItem,ValuesItem};
                    IID myid(types[row], parentId.resultId, false);
                    return createIndex(row, column, myid.uint());
                }
            }
            break;
        case AdviceItem:
        case PofIItem:
        case QofIOItem:
        case QofIOprimeItem:
        case OeqOprimeItem:
            break;
        case ValuesItem:{
                vector< PDTVar *> & vars = cSpecMW.resultVars[parentId.resultId];
                if (row < vars.size()) {
                    IID myid(VarItem,parentId.resultId,parentId.withCode, row);
                    return createIndex(row, column, myid.uint());
                } }
                break;
        case VarItem:
                break;
    }
    return QModelIndex();
}
#endif

#if 1
string SpecItemModel::getString(PDTNode * node) const {
    stringstream ss;
    node->toString(ss);
    return ss.str();
}

PDTSpecTriple* SpecItemModel::getSpecTriple(unsigned int row) const 
{
    SpecTripleMap::iterator it = cSpecMW.stMap.begin();
    unsigned int i =0;
    for (; it!=cSpecMW.stMap.end(); it++) {
        if (row == i) {
            return &(it->second);
        }
        i++;
    }
    return NULL;
}

QVariant SpecItemModel::headerData(int section, Qt::Orientation orientation, int role ) const{
    if (orientation == Qt::Horizontal && role == Qt::DisplayRole)
    {
        if (section == 0)
            return QVariant("Label");
        if (section == 1)
            return QVariant("Text");
#if 0
        if (section == 2)
            return QVariant("Value");
#endif
    }
    return QVariant();
}

int SpecItemModel::columnCount(const QModelIndex &parent ) const{
    return 2;
}

int 
SpecItemModel::rowCount(const QModelIndex &parent ) const {
    if (!parent.isValid())
        return cSpecMW.stMap.size();
    PDTNode * node = (PDTNode *)parent.internalId();
    if (node == NULL) {
        // this means that it is a pre/post or behavior that does not exist!
        return 0;
    }
    if (node->isSpecTriple()) {
        PDTSpecTriple*spec=dynamic_cast<PDTSpecTriple*>(node);
        return spec->numChildren() ;
    }
    if (node->isPreCondition())
        return 0;
    if (node->isPostCondition())
        return 0;
    if (node->isBehaviors()) {
        PDTBehaviors * behaviors = dynamic_cast<PDTBehaviors*>(node);
        return behaviors->getNumBehaviors();
    }
    if (node->isBehavior()) {
        return 2;//good, bad!
    }
    return 0;
}

QModelIndex SpecItemModel::makeParentSpecIdxModel(const string & name) const
{
    PDTSpecTriple & spec = cSpecMW.stMap[name];
    SpecTripleMap::iterator it = cSpecMW.stMap.begin();
    unsigned int row = 0;
    for (; it!=cSpecMW.stMap.end(); it++) {
        if (it->second == spec) 
            break;
        row++;
    }
    if (row <cSpecMW.stMap.size()) {
        return createIndex(row, 0, &spec);
    }
    return QModelIndex();
}


QModelIndex SpecItemModel::parent(const QModelIndex &index) const 
{
    if (!index.isValid())
        return QModelIndex();
    PDTNode * node = (PDTNode*)index.internalId();
    if (node == NULL){
        return QModelIndex();
    }
    if (node->isSpecTriple()) {
        return QModelIndex();
    } else if (node->isPreCondition()) {
        PDTPreCondition * pre = dynamic_cast<PDTPreCondition*>(node);
        string str = pre->getName();
        return makeParentSpecIdxModel(str);
    } else if (node->isPostCondition()) {
        PDTPostCondition * post = dynamic_cast<PDTPostCondition*>(node);
        string str = post->getName();
        return makeParentSpecIdxModel(str);
    } else if (node->isBehaviors()) {
        PDTBehaviors * behaviors = dynamic_cast<PDTBehaviors*>(node);
        string str = behaviors->getName();
        return makeParentSpecIdxModel(str);
    } else if (node->isBehavior()) {
        vector<PDTNode * > & parents = node->getParents();
        PDTBehaviors * behaviors = dynamic_cast<PDTBehaviors*>(parents[0]);
        string str = behaviors->getName();
        return createIndex(2, 0, behaviors);
    } else if (node->isStatement()) {
        vector<PDTNode * > & parents = node->getParents();
        PDTBehavior * beh = dynamic_cast<PDTBehavior*>(parents[0]);

        vector<PDTNode * > & ancestors = beh->getParents();
        PDTBehaviors * behaviors =  dynamic_cast<PDTBehaviors*>(ancestors[0]);
        unsigned int i = 0;
        for (; i < behaviors->getNumBehaviors();i++){
            PDTBehavior * bI = behaviors->getBehavior(i);
            if (beh == bI) {
                break;
            }
        }
        if (i < behaviors->getNumBehaviors()) {
            return createIndex(i, 0, beh);
        }
    }
    return QModelIndex();
}

Qt::ItemFlags SpecItemModel::flags(const QModelIndex &index) const
{
    if (!index.isValid())
        return 0;

    return Qt::ItemIsEnabled | Qt::ItemIsSelectable;
}


QVariant SpecItemModel::data(const QModelIndex &index, int role) const
{
    if (!index.isValid())
        return QVariant();

    if (role != Qt::DisplayRole)
        return QVariant();
    if (index.column() > 1) 
        return QVariant();

    PDTNode * node = (PDTNode*)index.internalId();
    if (node == NULL) 
        return QVariant();

    if (node->isSpecTriple()) {
        if (index.column() == 0) {
            PDTSpecTriple * spec = dynamic_cast<PDTSpecTriple*>(node);
            string name = spec->name();
            return QVariant(name.c_str());
        }
    } else  if (node->isPreCondition()) {
        // the following is true unless one does not exist!
   //level = 1, row = 0: pre item
   //level = 1, row = 1: post item
   //level = 1, row = 2: behaviors item
//        assert(index.row() == 0);
        if (index.column() == 0) {
            return QVariant("P:");
        } else if (index.column() == 1) {
            string str = getString(node);
            return QVariant(str.c_str());
        }
    } else if (node->isPostCondition()) {
//        assert(index.row() == 1);
        if (index.column() == 0) {
            return QVariant("Q:");
        } else if (index.column() == 1) {
            string str = getString(node);
            return QVariant(str.c_str());
        }
    } else if (node->isBehaviors()) {
//        assert(index.row() == 2);
        if (index.column() == 0) {
            return QVariant("Behaviors");
        }
    } else if (node->isBehavior()) {
        //if (index.row() < specTriple->behaviors->getNumBehaviors())
        PDTBehavior * beh = dynamic_cast<PDTBehavior*>(node);
        if (index.column() == 0) {
            if (beh->isGood()){
                return QVariant("Good");
            } else {
                return QVariant("Bad");
            }
        } else if (index.column() == 1) {
            return QVariant(index.row());
        }
    } else if (node->isStatement()) {
        vector<PDTNode * > & parents = node->getParents();
        PDTBehavior * beh = dynamic_cast<PDTBehavior*>(parents[0]);
        if (index.row() == 0) {
            if (index.column() == 0) {
                return QVariant("i:");
            } else if (index.column() == 1) {
                stringstream ss;
                beh->inToString(ss);
                return QVariant(ss.str().c_str());
            }
        } else if (index.row() == 1) {
            if (index.column() == 0) {
                return QVariant("o:");
            } else if (index.column() == 1) {
                stringstream ss;
                beh->outToString(ss);
                return QVariant(ss.str().c_str());
            }
        }
    }
    return QVariant();
}

QModelIndex SpecItemModel::index(int row, int column,
        const QModelIndex &parent ) const 
{
    if (!hasIndex(row, column, parent))
        return QModelIndex();

    if (column >= 2) 
        return QModelIndex();

    if (!parent.isValid()) {
        if (row < cSpecMW.stMap.size()) {
            void * p = (void*) getSpecTriple(row);
            return createIndex(row, column, p);
        }
        return QModelIndex();
    }

    PDTNode * node = (PDTNode*)parent.internalId();
#if 0
    if (node == NULL) {
        if (row < cSpecMW.stMap.size()) {
            void * p = (void*) getSpecTriple(row);
            return createIndex(row, column, p);
        }
        return QModelIndex();
    }
#endif
    if (node->isSpecTriple()) {
        PDTSpecTriple* spec = dynamic_cast<PDTSpecTriple*>(node);
        if ( row < spec->numChildren() ){
            PDTNode * idNode = spec->getNodeFromRow(row);
            if (idNode == NULL) {
                return QModelIndex();
            }
            return createIndex(row, column, idNode);
        }
    } else if (node->isPreCondition()) {
        return  QModelIndex();
        //return createIndex(row, column, (void*)NULL);
    } else if (node->isPostCondition()) {
        return  QModelIndex();
    } else if (node->isBehaviors()) {
        PDTBehaviors * behaviors = dynamic_cast<PDTBehaviors*>(node);
        if (row < behaviors->getNumBehaviors()) {
            PDTBehavior * beh = behaviors->getBehavior(row);
            return createIndex(row, column, beh);
        }
    } else if (node->isBehavior()) {
        PDTBehavior * beh = dynamic_cast<PDTBehavior*>(node);
        if (row == 0) {
            PDTStatement* statement = beh->getInputAssignment(0);
            return createIndex(row, column, statement);
        } else if (row == 1) {
            PDTStatement* statement = beh->getOutputAssignment(0);
            return createIndex(row, column, statement);
        }
    }
    return QModelIndex();
}

#endif

PDTCheckSpecMainWindow::PDTCheckSpecMainWindow() :
    cg(NULL), sCheck(NULL), sIModel(NULL), rIModel(NULL)
{
    codeEdit = new QTextEdit;
    setCentralWidget(codeEdit);

    createActions();

    createMenus();
    createToolBars();
    createStatusBar();
    createDockWindows();

    setWindowTitle(tr("Spec Check ! "));

//    newFile();
    setUnifiedTitleAndToolBarOnMac(true);
}

PDTCheckSpecMainWindow::~PDTCheckSpecMainWindow()
{
    clean();
}

void PDTCheckSpecMainWindow::setText(const QString & fname) {
    fileName = fname;
    codeEdit->clear();
    openFileEx();
}

void PDTCheckSpecMainWindow::newFile()
{
    codeEdit->clear();

    QTextCursor cursor(codeEdit->textCursor());
    cursor.movePosition(QTextCursor::Start);
    QTextFrame *topFrame = cursor.currentFrame();
    QTextFrameFormat topFrameFormat = topFrame->frameFormat();
    //topFrameFormat.setPadding(16);
    //topFrame->setFrameFormat(topFrameFormat);

    QTextCharFormat textFormat;
    QTextCharFormat boldFormat;
    boldFormat.setFontWeight(QFont::Bold);
    QTextCharFormat italicFormat;
    italicFormat.setFontItalic(true);

    fileName = "";
    if (cg) {
        delete cg;
        cg = NULL;
    }
    if (sCheck) {
        delete sCheck;
        sCheck = NULL;
    }

#if 0

    QTextTableFormat tableFormat;
    tableFormat.setBorder(1);
    tableFormat.setCellPadding(16);
    tableFormat.setAlignment(Qt::AlignRight);
    cursor.insertTable(1, 1, tableFormat);
    cursor.insertText("The Firm", boldFormat);
    cursor.insertBlock();
    cursor.insertText("321 City Street", textFormat);
    cursor.insertBlock();
    cursor.insertText("Industry Park");
    cursor.insertBlock();
    cursor.insertText("Some Country");
    cursor.setPosition(topFrame->lastPosition());
    cursor.insertText(QDate::currentDate().toString("d MMMM yyyy"), textFormat);
    cursor.insertBlock();
    cursor.insertBlock();
    cursor.insertText("Dear ", textFormat);
    cursor.insertText("NAME", italicFormat);
    cursor.insertText(",", textFormat);
    for (int i = 0; i < 3; ++i)
        cursor.insertBlock();
    cursor.insertText(tr("Yours sincerely,"), textFormat);
    for (int i = 0; i < 3; ++i)
        cursor.insertBlock();
    cursor.insertText("The Boss", textFormat);
    cursor.insertBlock();
    cursor.insertText("ADDRESS", italicFormat);
#endif
}


void 
PDTCheckSpecMainWindow::openFileEx() 
{
    //TODO: check if changes have not been saved
    //      and prompt user 

    QFile file(fileName);
    if (!file.open(QFile::ReadWrite | QFile::Text)) {
        QMessageBox::warning(this, tr("SpecCheck! "),
                             tr("Cannot open file %1:\n%2.")
                             .arg(fileName)
                             .arg(file.errorString()));
        return;
    }

    QTextStream in(&file);
    QApplication::setOverrideCursor(Qt::WaitCursor);
    codeEdit->setPlainText(in.readAll());
    file.close();
    QApplication::restoreOverrideCursor();

    statusBar()->showMessage(tr("Opened file '%1'").arg(fileName), 2000);
}


void 
PDTCheckSpecMainWindow::openFile() 
{
    //TODO: check if changes have not been saved
    //      and prompt user 

    fileName = QFileDialog::getOpenFileName(this,
                        tr("Open file"), "~",
                        tr("code (*.c *.sc);; all files (* *.*)"));
    if (fileName.isEmpty())
        return;
    openFileEx();
}



void PDTCheckSpecMainWindow::save()
{
    if (fileName.isEmpty()){
        fileName = QFileDialog::getSaveFileName(this,
                tr("Choose a file name"), ".",
                tr("code (*.c *.sc);; all files (* *.*)"));
        if (fileName.isEmpty())
            return;
    }
    QFile file(fileName);
    if (!file.open(QFile::WriteOnly | QFile::Text)) {
        QMessageBox::warning(this, tr("SpecCheck!"),
                             tr("Cannot write file %1:\n%2.")
                             .arg(fileName)
                             .arg(file.errorString()));
        return;
    }

    QTextStream out(&file);
    QApplication::setOverrideCursor(Qt::WaitCursor);
    out << codeEdit->toPlainText();
    QApplication::restoreOverrideCursor();

    statusBar()->showMessage(tr("Saved '%1'").arg(fileName), 2000);
}



void PDTCheckSpecMainWindow::undo()
{
    QTextDocument *document = codeEdit->document();
    document->undo();
}

void PDTCheckSpecMainWindow::clean() 
{
    if (cg) {
        delete cg;
        cg = NULL;
    }
    if (sCheck) {
        delete sCheck;
        sCheck = NULL;
    }
}

extern PDTCodeGraph *
mini_main(const string & file);

void  PDTCheckSpecMainWindow::parse() 
{
    clean();
    if (fileName.isEmpty()) return;
    QApplication::setOverrideCursor(Qt::WaitCursor);
    cg = mini_main(fileName.toLatin1().constData());
    QApplication::restoreOverrideCursor();
    if (cg == NULL) {
        QMessageBox::warning(this, tr("SpecCheck!"),
                             tr("Compiler error reading file %1")
                             .arg(fileName));
        return;
    }
    for (unsigned int i = 0; i < cg->nodes.size(); i++) {
        PDTNode * node = cg->nodes[i];
        string name;
        if (node->isPreCondition()){
            PDTPreCondition* pre = dynamic_cast<PDTPreCondition*>(node);
            name = pre->getName();
            PDTSpecTriple & st = stMap[name];
            st.pre = pre;
        }
        if (node->isPostCondition()){
            PDTPostCondition* post = dynamic_cast<PDTPostCondition*>(node);
            name = post->getName();
            PDTSpecTriple & st = stMap[name];
            st.post = post;
        }
        if (node->isBehaviors()){
            PDTBehaviors* behaviors= dynamic_cast<PDTBehaviors*>(node);
            name = behaviors->getName();
            PDTSpecTriple & st = stMap[name];
            st.behaviors = behaviors;
        }
    }
    if(sIModel != NULL) 
        delete sIModel;
    sIModel = new SpecItemModel(*this);
    specTree->setModel(sIModel);
}


bool
PDTCheckSpecMainWindow :: getInfoFromNode(PDTNode * node,
        PDTSpecTriple *& spec, PDTFunctionDec * & func, PDTBehavior * & beh)
{
    while (true) {
        if (node == NULL)
            return false;
        if (node->isFunctionDec()) {
            func = dynamic_cast<PDTFunctionDec*>(node);
            break; //we are done and no need to traverse further!
        } else if (node->isSpecTriple()) {
            spec = dynamic_cast<PDTSpecTriple*>(node);
        } else if (node->isPreCondition()) {
            PDTPreCondition * pre = dynamic_cast<PDTPreCondition*>(node);
            string str = pre->getName();
            spec = &stMap[str];
        } else if (node->isPostCondition()) {
            PDTPostCondition * post = dynamic_cast<PDTPostCondition*>(node);
            string str = post->getName();
            spec = &stMap[str];
        } else if (node->isBehaviors()) {
            PDTBehaviors * behaviors = dynamic_cast<PDTBehaviors*>(node);
            string str = behaviors->getName();
            spec = &stMap[str];
        } else if (node->isBehavior()) {
            beh = dynamic_cast<PDTBehavior*>(node);
        } else if (node->isStatement()) {
        }
        vector<PDTNode *> & parents = node->getParents();
        if (parents.size() == 0) {
            break;
        }
        node = parents[0];
    }
    if (spec == NULL)
        return false;
    if (spec->behaviors == NULL)
        return false;
    if (beh == NULL) {
        if (spec->behaviors->getNumBehaviors() > 0) 
            beh = spec->behaviors->getBehavior(0);
    }
    return true;
}


void  PDTCheckSpecMainWindow::check() 
{ 
    QItemSelectionModel *   selections = specTree->selectionModel () ;
    if (selections == NULL) return;
    QModelIndexList selectedItems = selections->selectedRows();
    if (selectedItems.isEmpty() ) {
        QMessageBox::warning(this, 
                tr("SpecCheck! "),
                tr("No specification is selected. Please select "
                    "a behavior or a specification tuple."));
        return;
    }
    unsigned int i =0;
    for(;i < selectedItems.size(); i++) {
        QModelIndex & midx = selectedItems[i];
        PDTNode * node = (PDTNode*)midx.internalId();

        PDTSpecTriple *spec=NULL;
        PDTFunctionDec * func = NULL;
        PDTBehavior * beh = NULL;
        if ( !getInfoFromNode(node, spec, func, beh)) {
            QMessageBox::warning(this, 
                    tr("SpecCheck! "),
                    tr("Selection does not lead to a specification with a behavior"));
            return;
        }
        try {
            QApplication::setOverrideCursor(Qt::WaitCursor);
            if (sCheck == NULL) {
                sCheck = new PDTCheckSpec (*cg, 
                        func, spec->behaviors,
                        spec->pre, spec->post);
            } else {
                sCheck->setFunctionSpecTriple(func,  
                        spec->behaviors, spec->pre, spec->post);
            }
            PDTCheckSpec::Result rc = sCheck->checkPrePost(beh);
            results.push_back(rc);
            QApplication::restoreOverrideCursor();
        } catch ( PDTException & e) {
            QApplication::restoreOverrideCursor();
            QMessageBox::critical(this, 
                    tr("SpecCheck! "),
                    tr(e.str().c_str()),
                    QMessageBox::Yes | QMessageBox::No);
            cerr << e.str() << endl;
            return ;
        }

        resultVars.push_back(vector<PDTVar*>());
        resultValues.push_back(vector<PDTConst*>());
        vector<PDTVar*> & vars = resultVars[resultVars.size() - 1];
        vector<PDTConst*> & values = resultValues[resultValues.size() - 1];
        unsigned int i = 0;
        for (;i < cg->variables.size(); i++) {
            PDTVar * var = cg->variables[i];
            PDTNode * node = var->getNode();
            if (node == NULL) {
                cout << var->getName() << ": node is NULL." << endl;
                continue;
            }
            PDTConst * val = sCheck->getValue(node);
            if (val != NULL) {
                vars.push_back(var);
                values.push_back(val);
            }
        }
    }
    if (rIModel != NULL)
        delete rIModel;
    rIModel = new ResultItemModel(*this);
    resultTree->setModel(rIModel);
}

void  PDTCheckSpecMainWindow::checkCode() 
{ 
    QItemSelectionModel *   selections = specTree->selectionModel () ;
    if (selections == NULL) return;
    QModelIndexList selectedItems = selections->selectedRows();
    if (selectedItems.isEmpty() ) {
        QMessageBox::warning(this, 
                tr("SpecCheck! "),
                tr("No specification is selected. Please select "
                    "a behavior or a specification tuple."));
        return;
    }
    unsigned int i =0;
    for(;i < selectedItems.size(); i++) {
        QModelIndex & midx = selectedItems[i];
        PDTNode * node = (PDTNode*)midx.internalId();

        PDTSpecTriple *spec=NULL;
        PDTFunctionDec * func = NULL;
        PDTBehavior * beh = NULL;
        if ( !getInfoFromNode(node, spec, func, beh)) {
            QMessageBox::warning(this, 
                    tr("SpecCheck! "),
                    tr("Selection does not lead to a specification with a behavior"));
            return;
        }
        try {
            QApplication::setOverrideCursor(Qt::WaitCursor);
            if (sCheck == NULL) {
                sCheck = new PDTCheckSpec (*cg, 
                        func, spec->behaviors,
                        spec->pre, spec->post);
            } else {
                sCheck->setFunctionSpecTriple(func,  
                        spec->behaviors, spec->pre, spec->post);
            }
            PDTListOfStatements * list = NULL;
            unsigned int idx = 0;
            bool hasCode = sCheck->locateCodeBetweenPreAndPost(list, idx);
            if (!hasCode) {
                QMessageBox::warning(this, 
                    tr("SpecCheck! "),
                    tr("Selected specification has no code between pre and post."));
                return;
            }
            PDTCheckSpec::Result rc = sCheck->checkPreCodePost(beh,*list,idx);
            results.push_back(rc);
            QApplication::restoreOverrideCursor();
        } catch ( PDTException & e) {
            QApplication::restoreOverrideCursor();
            QMessageBox::critical(this, 
                    tr("SpecCheck! "),
                    tr(e.str().c_str()),
                    QMessageBox::Yes | QMessageBox::No);
            cerr << e.str() << endl;
            return ;
        }
        resultVars.push_back(vector<PDTVar*>());
        resultValues.push_back(vector<PDTConst*>());
        vector<PDTVar*> & vars = resultVars[resultVars.size() - 1];
        vector<PDTConst*> & values = resultValues[resultValues.size() - 1];
        unsigned int i = 0;
        for (;i < cg->variables.size(); i++) {
            PDTVar * var = cg->variables[i];
            PDTNode * node = var->getNode();
            if (node == NULL) {
                cout << var->getName() << ": node is NULL." << endl;
                continue;
            }
            PDTConst * val = sCheck->getValue(node);
            if (val != NULL) {
                vars.push_back(var);
                values.push_back(val);
            }
        }
    }
    if (rIModel != NULL) 
        delete rIModel;
    rIModel = new ResultItemModel(*this);
    resultTree->setModel(rIModel);
}

void PDTCheckSpecMainWindow::resultChanged (const QString &res)
{
}



void PDTCheckSpecMainWindow::behaviorChanged(const QString &beh)
{
}


void PDTCheckSpecMainWindow::about()
{
   QMessageBox::about(this, tr("About SpecCheck!"),
            tr("The <b>SpecCheck!</b> tool demonstrates a methodology "

               "to build correct software incrementally." 
               " This is brought to you by the Software Analysis Research Lab (SARLab) at the American University of Beirut."));
}

void PDTCheckSpecMainWindow::createActions()
{
    newFileAct = new QAction(QIcon("./images/new.png"), tr("&New File"), this);
    newFileAct->setShortcuts(QKeySequence::New);
    newFileAct->setStatusTip(tr("Create a new file"));
    connect(newFileAct, SIGNAL(triggered()), this, SLOT(newFile()));

    openFileAct = new QAction(QIcon("./images/open.png"), tr("&Open File"), this);
    openFileAct->setShortcuts(QKeySequence::Open);
    openFileAct->setStatusTip(tr("Open a file"));
    connect(openFileAct, SIGNAL(triggered()), this, SLOT(openFile()));

    saveAct = new QAction(QIcon("./images/save.png"), tr("&Save..."), this);
    saveAct->setShortcuts(QKeySequence::Save);
    saveAct->setStatusTip(tr("Save file"));
    connect(saveAct, SIGNAL(triggered()), this, SLOT(save()));

    undoAct = new QAction(QIcon("./images/undo.png"), tr("&Undo"), this);
    undoAct->setShortcuts(QKeySequence::Undo);
    undoAct->setStatusTip(tr("Undo the last editing action"));
    connect(undoAct, SIGNAL(triggered()), this, SLOT(undo()));

    parseAct = new QAction(QIcon("./images/parse.png"), tr("&parse"), this);
//    parseAct->setShortcuts(QKeySequence::parse);
    parseAct->setStatusTip(tr("Parse the file"));
    connect(parseAct, SIGNAL(triggered()), this, SLOT(parse()));

    checkAct = new QAction(QIcon("./images/check.png"), tr("&check"), this);
    //checkAct->setShortcuts(QKeySequence::check);
    checkAct->setStatusTip(tr("check {P}-{Q}{B} with the selected behavior"));
    connect(checkAct, SIGNAL(triggered()), this, SLOT(check()));

    checkCodeAct = new QAction(QIcon("./images/checkCode.png"), tr("check c&ode"), this);
    //checkCodeAct->setShortcuts(QKeySequence::checkCode);
    checkCodeAct->setStatusTip(tr("check {P}S{Q}{B} with the selected behavior"));
    connect(checkCodeAct, SIGNAL(triggered()), this, SLOT(checkCode()));

    quitAct = new QAction(tr("&Quit"), this);
    quitAct->setShortcuts(QKeySequence::Quit);
    quitAct->setStatusTip(tr("Quit the application"));
    connect(quitAct, SIGNAL(triggered()), this, SLOT(close()));

    aboutAct = new QAction(tr("&About"), this);
    aboutAct->setStatusTip(tr("Show the application's About box"));
    connect(aboutAct, SIGNAL(triggered()), this, SLOT(about()));
}

void PDTCheckSpecMainWindow::createMenus()
{
    fileMenu = menuBar()->addMenu(tr("&File"));
    fileMenu->addAction(newFileAct);
    fileMenu->addAction(openFileAct);
    fileMenu->addAction(saveAct);
    fileMenu->addSeparator();
    fileMenu->addAction(quitAct);

    editMenu = menuBar()->addMenu(tr("&Edit"));
    editMenu->addAction(undoAct);

    checkMenu = menuBar()->addMenu(tr("&Check"));
    checkMenu->addAction(parseAct);
    checkMenu->addAction(checkAct);
    checkMenu->addAction(checkCodeAct);

    viewMenu = menuBar()->addMenu(tr("&View"));
    menuBar()->addSeparator();

    helpMenu = menuBar()->addMenu(tr("&Help"));
    helpMenu->addAction(aboutAct);
}

void PDTCheckSpecMainWindow::createToolBars()
{
    fileToolBar = addToolBar(tr("File"));
    fileToolBar->addAction(newFileAct);
    fileToolBar->addAction(openFileAct);
    fileToolBar->addAction(saveAct);

    editToolBar = addToolBar(tr("Edit"));
    editToolBar->addAction(undoAct);

    checkToolBar = addToolBar(tr("SpecCheck"));
    checkToolBar->addAction(parseAct);
    checkToolBar->addAction(checkAct);
    checkToolBar->addAction(checkCodeAct);
}


void PDTCheckSpecMainWindow::createStatusBar()
{
    statusBar()->showMessage(tr("Ready"));
}



void PDTCheckSpecMainWindow::createDockWindows()
{
    QDockWidget *dock = new QDockWidget(tr("{P}-{Q}{B} sets"), this);
    dock->setAllowedAreas(Qt::LeftDockWidgetArea | Qt::RightDockWidgetArea);
    specTree = new QTreeView (dock);
//    specTree->setWordWrap(true);
    specTree->setSelectionBehavior (QAbstractItemView::SelectRows);
    specTree->setSelectionMode (QAbstractItemView::SingleSelection);
    specTree->setAlternatingRowColors (true);
    dock->setWidget(specTree);
    addDockWidget(Qt::RightDockWidgetArea, dock);
//    addDockWidget(Qt::RightDockWidgetArea, dock);
    viewMenu->addAction(dock->toggleViewAction());

    dock = new QDockWidget(tr("Results"), this);
    dock->setAllowedAreas(Qt::AllDockWidgetAreas);
    resultTree = new QTreeView(dock);
    dock->setWidget(resultTree);
    //addDockWidget(Qt::BottomDockWidgetArea, dock);
    addDockWidget(Qt::RightDockWidgetArea, dock);
    viewMenu->addAction(dock->toggleViewAction());
}


